nLab geometric category

Redirected from "infinitary coherent category".
Contents

Contents

Definition

An infinitary coherent category or geometric category is a regular category in which the subobject posets Sub(X)Sub(X) have all small unions which are stable under pullback.

More generally, for κ\kappa a regular cardinal, a κ\kappa-geometric category, or κ\kappa-coherent category, is a regular category with unions for κ\kappa-small families of subobjects, stable under pullback. (For κ=ω\kappa = \omega this reduces to the notion of coherent category, called a pre-logos by Freyd–Scedrov.)

Makkai-Reyes call this a κ\kappa-logical category, while Shulman calls it a κ\kappa-ary regular category. See also (Butz-Johnstone, p. 12).

Properties

See familial regularity and exactness for a general description of the spectrum from regular categories through finitary and infinitary coherent categories.

Well-poweredness

Frequently, geometric categories are additionally required to be well-powered. If a geometric category is well-powered, then its subobject posets are complete lattices, hence also have all intersections. Moreover, by the adjoint functor theorem for posets, it is a Heyting category.

However, since geometric logic does not include implication or infinite conjunction, this categorical structure should not necessarily be expected to exist in a category called “geometric” (and when they do exist, they are not preserved by geometric functors). A requirement of well-poweredness is also inconsistent with the spectrum of familial regularity and exactness.

Note, however, that if a geometric category has a small generating set, then it is necessarily well-powered. In particular, this applies to the syntactic category of any (small) geometric theory, and also to any Grothendieck topos.

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus

References

Around lemma A1.4.18 in

  • Casten Butz, Peter Johnstone, Classifying toposes for first order theories, BRICS Report Series RS-97-20

Last revised on November 16, 2022 at 05:59:31. See the history of this page for a list of all contributions to it.